Groth16 Batch Verification

7 March 2024 (updated 7 March 2024)

$$ \gdef\delim#1#2#3{\mathopen{}\mathclose{\left#1 #2 \right#3}} \gdef\p#1{\delim({#1})} \gdef\set#1{\delim\{{#1}\}} \gdef\e{\operatorname{e}} \gdef\g{\mathrm{g}} \gdef\Z{\mathrm{Z}} \gdef\U{\mathrm{U}} \gdef\V{\mathrm{V}} \gdef\W{\mathrm{W}} \gdef\k#1{\mathbf{#1}} \gdef\F{\mathbb{F}} \gdef\G{\mathbb{G}} \gdef\ga#1{\delim[{#1}]_1} \gdef\gb#1{\delim[{#1}]_2} $$

Introduction

Constraints

Recall Groth16. For a given circuit with $n$ variables, $m$ constraints and $p$ public inputs we encode the circuit as $3⋅n+1$ polynomials $\U_i, \V_i, \W_i, \Z ∈ \F[X]$ each with $m$ terms (i.e. degree $m-1$). A witness $x ∈\F^n$ is correct if for some $H(X) ∈ \F[X]$ it satisfies

$$ \p{\sum_{i∈[0,n)} x_i ⋅ \U_i(X)} ⋅ \p{\sum_{i∈[0,n)} x_i ⋅ \V_i(X)} = \p{\sum_{i∈[0,n)} x_i ⋅ \W_i(X)} + H(X) ⋅\Z(X) $$

For a given circuit and setup we have $\ga{α}, \gb{β}, L_i, \gb{γ}, \ga{δ}$.

Consider a proof $(x_i, A, B, C)$. To verify it we check

$$ 0 = \e\p{A, B} - \e\p{\ga{α}, \gb{β}} - \e\p{\sum_{i∈[0,p)}x_i⋅L_i, \gb{γ}} - \e\p{C, \gb{δ}} $$

Linear combinations

Consider many proofs $(x_{ij}, A_j, B_j, C_j)$. Take a random linear product of verifications with $r_j ∈ \F$.

$$ \begin{aligned} 0 &= \sum_j r_j⋅ \p{\e\p{A_j, B_j} -\e\p{\ga{α}, \gb{β}} - \e\p{\sum_{i∈[0,p)}x_{ij}⋅L_i, \gb{γ}} - \e\p{C_j, \gb{δ}} }\\ &= \sum_j r_j⋅ \e\p{A_j, B_j} - \e\p{\sum_j r_j⋅\ga{α}, \gb{β}}- \e\p{\sum_{i∈[0,p)}\p{\sum_j x_{ij}⋅r_j}⋅L_i, \gb{γ}} - \e\p{\sum_j r_j⋅C_j, \gb{δ}} \end{aligned} $$

The problem is $\sum_j r_j⋅ \e\p{A_j, B_j}$ is not computable in $\G_1, \G_2$ but requires operations in $\G_3$.

If we simply forced the sum inside we'd get many cross terms:

$$ \begin{aligned} \e\p{\sum_j r_j⋅ A_j, \sum_j r_j⋅ B_j} &= \sum_i \sum_j r_i⋅ r_j⋅ \e\p{A_i, B_j} \end{aligned} $$

Snarkpack solves this using a target inner pairing product (TIPP) protocol to provide the verifier with $\sum_j r_j⋅ \e\p{A_j, B_j}$ and proof that it was constructed correctly.

Attempt at alternative

What if instead we embrace the cross terms and try to make it work?

$$ \begin{aligned} \e\p{\sum_j r^j⋅ A_j, \sum_j s_j⋅ B_j} &= \sum_i \sum_j r^i⋅ s_j⋅ \e\p{A_i, B_j} \end{aligned} $$

Poor man's snarkpack

We can also simply not aggregate the $\e{A,B}$ pair:

$$ \begin{aligned} \sum_j \e\p{r^j⋅ A_j, B_j} &= \e\p{\sum_j r^j⋅\ga{α}, \gb{β}} + \e\p{\sum_{i∈[0,p)}\p{\sum_j x_{ij}⋅r^j}⋅L_i, \gb{γ}} + \e\p{\sum_j r^j⋅C_j, \gb{δ}} \end{aligned} $$

This should trivially work and save 75% of the pairings, at the cost of $\F$ and $\G_1$ operations.

Poor man's turbo

The aggregator computes

$$ \begin{aligned} C &= \sum_j r^j ⋅ C_j \\ \end{aligned} $$

The verifier checks

$$ \begin{aligned} \sum_j \e\p{r^j⋅ A_j, B_j} &= \e\p{\p{\sum_j r^j}⋅\ga{α}, \gb{β}} + \e\p{\sum_{i∈[0,p)}\p{\sum_j x_{ij}⋅r^j}⋅L_i, \gb{γ}} + \e\p{C, \gb{δ}} \end{aligned} $$

This requires $2⋅(n-1)$ times $\mathsf{Add}_{\F}$, $p⋅n$ times $\mathsf{Mul}_{\F}$, $n+p+1$ times $\mathsf{Mul}_{\G_1}$ and $n+3$ times $\mathsf{Pair}$.

This construction preserves completeness and zero-knowledge, but does it preserve soundness?

Note. If this works it could also be applied to SnarkPack.

Attempted Soundness Proof

As before, but now with additional formal parameters $r_j$.

$$ \begin{aligned} \sum_j r^j⋅ A_j⋅ B_j &= \sum_j r^j⋅α⋅β + \sum_j r^j ⋅\sum_{i∈[0,p)} x_{ij}⋅\p{β⋅\U_i(τ)+α⋅\V_i(τ)+\W_i(τ)} +C⋅δ \end{aligned} $$

where we have multiple $A, B$ values

$$ \begin{aligned} A_j &= A_{τj}(τ) + A_{αj}(τ)⋅α + A_{βj}(τ)⋅β + A_{δj} ⋅ δ + A_{γj} ⋅ γ + A_{Zj}(τ)⋅{\footnotesize \frac{\Z(τ)}{δ}} \\[0.5em] &\phantom{=}+ \sum_{i∈[0,p)} A_{ij}⋅{\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ}} + \sum_{i∈[p,m)} A_{ij}⋅ {\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{δ} } \\[2em] B_j &= B_{τj}(τ) + B_{βj}⋅β + B_{δj} ⋅ δ + B_{γj} ⋅ γ \\[0.2em] \end{aligned} $$

The aggregator constructs a $C$ while having knowledge of the $r_j$:

$$ \begin{aligned} C &= C_τ(r, τ) + C_α(r, τ)⋅α + C_β(r,τ)⋅β + C_δ(r) ⋅ δ + C_γ(r) ⋅ γ + C_Z(r,τ)⋅{\footnotesize \frac{\Z(τ)}{δ}} \\[0.5em] &\phantom{=}+ \sum_{i∈[0,p)} C_i(r)⋅{\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ}} + \sum_{i∈[p,m)} C_i(r)⋅ {\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{δ} } \end{aligned} $$

Where each function $f(r, τ)$ can is of the form $f_0(r) + f_1(r)⋅τ + f_2(r)⋅τ^2+⋯$.

The steps where the RHS is constant factor on $r$ and are much the same as before:

$$ \begin{aligned} A_{αj}(τ) ⋅ B_{βj} &= 1 &\hspace{2em}&\p{α⋅β⋅τ^i⋅r^j} \\ A_{βj}(τ) ⋅ B_{βj} &= 0 &\hspace{2em}&\p{β^2⋅τ^i⋅r^j} \\ A_{αj}(τ) ⋅ B_{γj} &= 0 &\hspace{2em}&\p{α⋅γ⋅τ^i⋅r^j} \\ &\hspace{0.7em}⋮ \end{aligned} $$

So we again get

$$ \begin{aligned} A_j &= A_{τj}(τ) + A_{αj}⋅α + A_{δj} ⋅ δ \\ B_j &= B_{τj}(τ) + A_{αj}^{-1} ⋅ β + B_{δj} ⋅ δ \end{aligned} $$

Looking at monomials

$$ \begin{aligned} \sum_j r^j ⋅ A_{αj} ⋅ B_{τj}(τ) &= \sum_j \sum_{i∈[0,p)} r^j⋅x_{ij} ⋅ \V_i(τ) + \sum_{i∈[p,m)} C_i(r) ⋅ \V_i(τ) &\hspace{2em}&\p{α⋅τ^i⋅r^j} \\ \sum_j r^j ⋅ A_{αj}^{-1} ⋅ A_{τj}(τ) &= \sum_j \sum_{i∈[0,p)} r^j⋅x_{ij} ⋅ \U_i(τ) + \sum_{i∈[p,m)} C_i(r) ⋅ \U_i(τ) &\hspace{2em}&\p{β⋅τ^i⋅r^j} \end{aligned} $$

Defining

$$ \hat x_i =\begin{cases} \sum_j r^j ⋅ x_{ij} & i∈[0,p) \\ C_i(r) & i∈[p,m) \end{cases} $$

we can rewrite these as

$$ \begin{aligned} \sum_j r^j ⋅ A_{αj} ⋅ B_{τj}(τ) &= \sum_{i∈[0,m)} \hat x_i ⋅ \V_i(τ) \\ \sum_j r^j ⋅ A_{αj}^{-1} ⋅ A_{τj}(τ) &= \sum_{i∈[0,m)} \hat x_i ⋅ \U_i(τ) \end{aligned} $$

Finally looking at the monomials in $τ^i⋅r^j$:

$$ \begin{aligned} \sum_j r^j ⋅ A_{τj}(τ) ⋅ B_{τj}(τ) &= \sum_j r^j ⋅\sum_{i∈[0,p)} x_{ij}⋅\W_i(τ) + \sum_{i∈[p,m)} C_i(r)⋅\W_i(τ) + C_Z(r,τ)⋅\Z(τ) \end{aligned} $$

Simplifiying using $\hat x$

$$ \begin{aligned} \sum_j r^j ⋅ A_{τj}(τ) ⋅ B_{τj}(τ) &= \sum_{i∈[0,p)} \hat x_i⋅\W_i(τ) + C_Z(r,τ)⋅\Z(τ) \end{aligned} $$

Looking at the left hand side:

$$ \begin{aligned} \sum_j r^j ⋅ A_{τj}(τ) ⋅ B_{τj}(τ) &= \end{aligned} $$

Assume for the moment $\U_i, \V_i, \W_i$ are all linearly independent Then

We are looking for

$$ \sum_{j∈[0,k)} r^j⋅ \p{\sum_{i∈[0,n)} x_{ij} ⋅ \U_i(X)} ⋅ \p{\sum_{i∈[0,n)} x_{ij} ⋅ \V_i(X)} = \sum_{\substack{i∈[0,n)\\j∈[0,k)}} r^j ⋅ x_{ij} ⋅ \W_i(X) + \sum_j r^j ⋅ H_j(X) ⋅\Z(X) $$

Question. Can we define $H(X) = \sum_j r^j ⋅ H(X)$ and forgo breaking it down?

$$ \sum_{j∈[0,k)} r^j⋅ \p{\sum_{i∈[0,n)} x_{ij} ⋅ \U_i(X)} ⋅ \p{\sum_{i∈[0,n)} x_{ij} ⋅ \V_i(X)} = \sum_{\substack{i∈[0,n)\\j∈[0,k)}} r^j ⋅ x_{ij} ⋅ \W_i(X) + H(X) ⋅\Z(X) $$